feat(Combinatorics): link `Nat.Partition` to `YoungDiagram` by kg583 · Pull Request #39722 · leanprover-community/mathlib4

kg583 · 2026-05-22T20:11:30Z

AI disclosure: Claude was used to source some proof sketches.

github-actions · 2026-05-22T20:11:41Z

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

github-actions · 2026-05-22T20:12:44Z

PR summary 8f7e4fe3b7

Import changes exceeding 2%

%	File
+3.75%	`Mathlib.Combinatorics.Young.YoungDiagram`

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Combinatorics.Young.YoungDiagram	533	553	+20 (+3.75%)

Import changes for all files

Files	Import difference
`Mathlib.Combinatorics.Young.SemistandardTableau` `Mathlib.Combinatorics.Young.YoungDiagram`	20
`Mathlib.Combinatorics.Enumerative.Partition.YoungDiagram` (new file)	722

Declarations diff (regex)

+ card_ofPartition
+ card_transpose
+ conjugate
+ conjugate_conjugate
+ equivPartition
+ ofPartition
+ ofPartition_toPartition
+ rowLens_ofPartition_eq_sort_parts
+ sum_rowLens_eq_card
+ toPartition
+ toPartition_ofPartition

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 8f7e4fe).

+12 new declarations
−0 removed declarations

+Nat.Partition.conjugate
+Nat.Partition.conjugate_conjugate
+YoungDiagram.card_ofPartition
+YoungDiagram.card_transpose
+YoungDiagram.equivPartition
+YoungDiagram.ofPartition
+YoungDiagram.ofPartition_toPartition
+YoungDiagram.rowLens_ofPartition_eq_sort_parts
+YoungDiagram.sum_rowLens_eq_card
+YoungDiagram.toPartition
+YoungDiagram.toPartition.congr_simp
+YoungDiagram.toPartition_ofPartition

No changes to strong technical debt.

Increase in weak tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type (weak)
4974	1	exposed public sections

Current commit 8f7e4fe3b7
Reference commit 8d0d1cff7b

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

wwylele

Mostly comments on naming convention

kg583 · 2026-05-22T23:19:12Z

Thank you for the review @wwylele. Questions for my own edification:

Moving the lemma to the YoungDiagram API required additional imports for some theorems, but imports that I had to cross reference a docs search to find the exact origin of, and ones which did not nominatively match those in Partition/Basic due to transitive imports. How should one identify the "proper" import targets?
Said lemma is now the only lemma in that file, everything else being a theorem. I understand that these are functionally identical designations, but how ought one delineate when working across multiple files with differing internal conventions?

wwylele · 2026-05-23T00:25:23Z

If I understand the question correctly, when adding imports, I would import the file that directly contains the theorem I want to use.
I don't know if there is a guideline for this. It is probably just vibe-dependent

wwylele

Mostly minor golfing. I don't have other comments

wwylele · 2026-05-23T01:00:59Z

+    (p.parts.sort (· ≥ ·)).sum
+      = (↑(p.parts.sort (· ≥ ·)) : Multiset ℕ).sum := Multiset.sum_coe _
+    _ = p.parts.sum := by rw [Multiset.sort_eq]


This part feels like a missing lemma ((?a : Multiset a).sort ?b).sum = (?a : Multiset a).sum that we should extract out

Where would this ideally go?

What does #find_home suggest? (See find_home)

#find_home suggests [Mathlib.Combinatorics.Enumerative.Composition]

NoahW314

Glad to see this is getting done!

I'm a little hesitant to place all of this in Partition/Basic since many other files import it as well. However, I do see the point of having conjugate defined here. Perhaps it would be better to move the equivalence to YoungDiagram (since this is essentially a leaf file) and then make a new file under Partition/ for conjugate?

Do we want this equivalence to be toYoungDiagram/ofYoungDiagram or toPartition/ofPartition? To me the latter seems more natural, but I'm curious to know what other people think.

Co-authored-by: Weiyi Wang <wwylele@gmail.com> Co-authored-by: Noah Walker <noahwalker3.14@gmail.com>

kg583 · 2026-05-23T03:37:16Z

I'm a little hesitant to place all of this in Partition/Basic since many other files import it as well. However, I do see the point of having conjugate defined here. Perhaps it would be better to move the equivalence to YoungDiagram (since this is essentially a leaf file) and then make a new file under Partition/ for conjugate?

Yeah, I'm down for this approach, as the equivalence isn't really the important part here.

Do we want this equivalence to be toYoungDiagram/ofYoungDiagram or toPartition/ofPartition? To me the latter seems more natural, but I'm curious to know what other people think.

I am biased as a number theorist, but converting a partition to a Young diagram to then perform some useful operation (e.g. conjugating, computing partition statistics, finding t-hooks) is "the" natural direction, seemingly more so than the other way around. That said, future modules that do these sorts of things don't actually have to care about this API direction, at least to the end user.

NoahW314 · 2026-05-23T03:52:12Z

I'm a little hesitant to place all of this in Partition/Basic since many other files import it as well. However, I do see the point of having conjugate defined here. Perhaps it would be better to move the equivalence to YoungDiagram (since this is essentially a leaf file) and then make a new file under Partition/ for conjugate?

Yeah, I'm down for this approach, as the equivalence isn't really the important part here.

Sorry, my original comment was poorly worded. To be clear, I'm suggesting moving everything to YoungDiagram to avoid importing YoungDiagram in Partition/Basic (and perhaps putting conjugate in a new file so that it can remain in the Partition/ folder).

kg583 · 2026-05-23T19:16:09Z

Sorry, my original comment was poorly worded. To be clear, I'm suggesting moving everything to YoungDiagram to avoid importing YoungDiagram in Partition/Basic (and perhaps putting conjugate in a new file so that it can remain in the Partition/ folder).

Implemented this since I agree that it makes the API and imports generally cleaner. Partition/Conjugate is also a good place to put some simple theorems like (# of partitions with max part m) = (# of partitions with length m) (happy to do in this PR but also happy to wait).

NoahW314 · 2026-05-24T01:45:35Z

Partition/Conjugate is also a good place to put some simple theorems like (# of partitions with max part m) = (# of partitions with length m) (happy to do in this PR but also happy to wait).

Doing this in a later PR would be great!

wwylele

Just one comment on the doc

wwylele

Sorry, I missed one small thing

Co-authored-by: Weiyi Wang <wwylele@gmail.com>

YaelDillies · 2026-06-26T07:52:30Z


+@[simp]
+lemma card_transpose (μ : YoungDiagram) : μ.transpose.card = μ.card := by
+  simp [transpose, YoungDiagram.card]


Suggested change

simp [transpose, YoungDiagram.card]

simp [transpose, card]

or is that protected/ambiguous?

The abbreviation is protected (L181).

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

…iagram

YaelDillies · 2026-06-26T20:02:50Z

For me it would make sense to make a file under Partition about the connection to Young diagrams, rather than chucking that in the basic YoungDiagram file, then this very short file needn't exist

I intend to add some useful definitions and bijections concerning specifically conjugation in the future that would have made it less of a stub file, though I agree that the equivalence can naturally live in Partition.

Should the "direction" of the equivalences be changed as well? i.e. Nat.Partition.toYoungDiagram ?

YaelDillies · 2026-06-26T20:08:37Z

+  rw [← sum_rowLens_eq_card, rowLens_ofPartition_eq_sort_parts]
+  calc
+    (p.parts.sort (· ≥ ·)).sum
+      = (↑(p.parts.sort (· ≥ ·)) : Multiset ℕ).sum := Multiset.sum_coe _
+    _ = p.parts.sum := by rw [Multiset.sort_eq]
+    _ = n := p.parts_sum


Suggested change

rw [← sum_rowLens_eq_card, rowLens_ofPartition_eq_sort_parts]

calc

(p.parts.sort (· ≥ ·)).sum

= (↑(p.parts.sort (· ≥ ·)) : Multiset ℕ).sum := Multiset.sum_coe _

_ = p.parts.sum := by rw [Multiset.sort_eq]

_ = n := p.parts_sum

rw [← sum_rowLens_eq_card, rowLens_ofPartition_eq_sort_parts, List.sort_perm.sum_eq, p.parts_sum]

where sort_perm is a (missing?! surely I overlooked it) lemma saying l.sort _ is a permutation of l

LeanSearch finds some close misses, such as List.perm_insertionSort. I'm unsure the best way to decide on a refactor given none of the options are quite right.

NoahW314 · 2026-07-06T20:10:25Z

@kg583 As a reminder, you can type -awaiting-author to remove the awaiting-author label if the PR is ready for review again (See lifecycle of a pr).

kg583 · 2026-07-06T20:23:33Z

-awaiting-author

kg583 added 5 commits May 20, 2026 12:25

Add YoungDiagram conversion

ad4e392

Add equivalence and conjugation

73823e2

Prefer implicit binder

a19cde8

Namespace nits

9b69192

Nits

1caea90

github-actions Bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label May 22, 2026

github-actions Bot added the t-combinatorics Combinatorics label May 22, 2026

wwylele reviewed May 22, 2026

View reviewed changes

kg583 added 2 commits May 22, 2026 18:00

Fix names

e7b7763

Move Young diagram lemma

2afbc10

github-actions Bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label May 22, 2026

wwylele reviewed May 23, 2026

View reviewed changes

NoahW314 reviewed May 23, 2026

View reviewed changes

kg583 and others added 2 commits May 22, 2026 22:25

Golfs

a54c616

Co-authored-by: Weiyi Wang <wwylele@gmail.com> Co-authored-by: Noah Walker <noahwalker3.14@gmail.com>

[pre-commit.ci lite] apply automatic fixes

fe6087d

Extract out transpose_card_eq_card

c182087

Move equivalence and split out Conjugate

d182b96

kg583 added 2 commits May 23, 2026 14:39

Additional @[simp]s

3905844

Add Conjugate to Mathlib

b1a5d07

NoahW314 reviewed May 24, 2026

View reviewed changes

Comment thread Mathlib/Combinatorics/Young/YoungDiagram.lean Outdated

Comment thread Mathlib/Combinatorics/Enumerative/Partition/Conjugate.lean Outdated

kg583 added 2 commits May 23, 2026 23:10

Remove selfConjugate def (for now)

15d77a8

Rename to card_transpose

a7c4321

wwylele approved these changes May 24, 2026

View reviewed changes

Comment thread Mathlib/Combinatorics/Young/YoungDiagram.lean Outdated

Redundant docstring

1fc2b96

wwylele reviewed May 24, 2026

View reviewed changes

Comment thread Mathlib/Combinatorics/Young/YoungDiagram.lean Outdated

Use direct subtype

3d512d8

Co-authored-by: Weiyi Wang <wwylele@gmail.com>

NoahW314 approved these changes May 26, 2026

View reviewed changes

mathlib-triage Bot assigned YaelDillies Jun 26, 2026

YaelDillies changed the title ~~feat(Combinatorics): Link Nat.Partition to YoungDiagram~~ feat(Combinatorics): link Nat.Partition to YoungDiagram Jun 26, 2026

YaelDillies reviewed Jun 26, 2026

View reviewed changes

kg583 and others added 2 commits June 26, 2026 12:19

Whitespace lint

8affb65

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Merge remote-tracking branch 'upstream/master' into partition-young-d…

487d6f1

…iagram

YaelDillies reviewed Jun 26, 2026

View reviewed changes

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Jun 26, 2026

kg583 added 3 commits July 1, 2026 17:25

Add @[simp]

a9e05b3

Remove rowLens_ofPartition_eq_parts

3bb7bcc

Move Young diagram definitions

8f7e4fe

github-actions Bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 6, 2026

Uh oh!

Conversation

kg583 commented May 22, 2026

Uh oh!

github-actions Bot commented May 22, 2026

Welcome new contributor!

Uh oh!

github-actions Bot commented May 22, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 8f7e4fe3b7

Import changes for modified files

Declarations diff (regex)

Declarations diff (Lean)

Uh oh!

wwylele left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

kg583 commented May 22, 2026

Uh oh!

wwylele commented May 23, 2026

Uh oh!

wwylele left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

NoahW314 left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

kg583 commented May 23, 2026

Uh oh!

NoahW314 commented May 23, 2026

Uh oh!

kg583 commented May 23, 2026

Uh oh!

Uh oh!

Uh oh!

NoahW314 commented May 24, 2026

Uh oh!

wwylele left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

wwylele left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

github-actions Bot commented May 22, 2026 •

edited

Loading